Designers of sequential digital circuits increasingly employ high level software languages to specify complex designs. For example, a given hardware model may have a high-level representation in VHDL or BESTMAP-C, which are hardware description languages. The designer may then employ software tools to develop an appropriate circuit design from the given high-level description or specification.
An important operation in this process is the verification or validation of the high-level specification. If the high-level specification contains inaccuracies or produces incongruous results, then the circuit designed therefrom will contain faults. To validate the specification, therefore, the designer must ensure that the set of all possible input configurations produces the proper response. One method of performing the validation step is to apply every possible input configuration to the high-level specification and observe the results. For designs of large complexity, and particularly for large sets of distinct input configurations, such a method is impractical.
Consider, for example, a given circuit specification that involves the manipulation of three non-negative integer variables, a, b and c, which may be, for example, counter values. Suppose the circuit designer is required to know the range of possible results given any initial starting point {a,b,c} where a&lt;20, b&lt;10 and c is unrestricted. In such a situation, executing each possible configuration of a, b and c individually would require a minimum of 200 executions and possibly significantly more, depending on the upper limit of possible values of c.
An alternative method of validating a specification, which involves employing the symbolic execution of state machine models, is disclosed in Coudert, et al., "Verification of Synchronous Sequential Machines Based on Symbolic Execution," Automatic Verification Methods for Finite State Systems, LNCS No. 407 (Springer Verlag 1990); and Dill, "Timing Assumptions and Verification of Finite-State Concurrent Systems," Automatic Verification Methods for Finite State Systems, LNCS No. 407 (Springer Verlag 1990), both of which are incorporated herein by reference. Coudert, et al., show how a high-level description may be executed symbolically to provide the set of reachable values from a particular set of input sequences. In this method, the high-level description is first converted into a state machine representation. Symbolical execution of the state machine then provides the set of reachable values or configurations.
Symbolic execution methods evaluate a particular model by executing the state machine using sets of configurations, as opposed to individual configurations. As a result, the use of symbolic execution can greatly reduce the time and effort needed for validation of a specification.
Consider again, for example, the system described above involving the integer variables a, b and c. In symbolic execution, the state machine model is executed once for the set of configurations of {a,b,c} where a&lt;20, b&lt;10 and c is unrestricted. Such a set is often referred to as a region. The use of the term region reflects the fact that sets of configurations given as linear functions or linear inequalities may be represented graphically as regions.
The results of the symbolic execution yield a cover, or a potentially redundant set, of the reachable configurations. The set of reachable configurations reveals to a circuit designer whether a prohibited configuration may possibly be reached under the model. If, for example, the cover includes the point {25, 28, 40}, and it is known that the point {25, 28, 40} would cause system error the designer becomes informed of a flaw in the high-level specification. In comparison, if each individual initial configuration of {a,b,c} within the initial region is separately executed, hundreds of possible starting points may have to be executed through the model before such an error point is reached.
Symbolic execution methods have been described for circuit specifications which are modelled using boolean variables and expressions in Coudert, et al, above. These known methods utilize binary decision diagram manipulation in order to effect symbolic execution on the state machine models. Additionally, symbolic execution methods have also been described for circuit specifications consisting of arithmetic variables, Dill, et al, above. Arithmetic variables, as opposed to Boolean variables, represent non-negative integers in sequential circuit models.
In some cases, however, a high-level specification or model may include both Boolean and arithmetic variables. Such models are known as hybrid models. A current technique of performing symbolic execution methods on hybrid models requires expanding the arithmetic variables and expressions to their Boolean equivalent representation. By representing all variables homogeneously as Boolean variables, the symbolic execution techniques discussed by Coudert, et al, above may be implemented.
The conversion of arithmetic variables to Boolean variables, however, introduces inefficiency, particularly in complex hybrid models. One particular problem in the Boolean expansion of arithmetic variables is that a maximum word size must be defined for each arithmetic variable to be expanded. For example, to expand an arithmetic variable "a" a designer must define a maximum value of "a" in order to determine how many Boolean variables must be created to replace it. For example, if the value of "a" is always less than 8, then a three bit or three variable Boolean expansion is adequate. If, however, the maximum value of "a" reaches 100, at least a seven bit or seven variable Boolean expansion is required.